\begin{tabbing}
es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=l{-}all(\=fpf{-}domain(${\it ds}$);\+\+
\\[0ex]$x$.let $T$ = fpf{-}ap(${\it ds}$; id{-}deq; $x$) in subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); $T$))
\-\\[0ex]$\wedge$ l{-}all(\=fpf{-}domain(${\it da}$);\+
\\[0ex]$k$.let \=$T$\= = fpf{-}ap(${\it da}$; Kind{-}deq; $k$) in\+\+
\\[0ex]$\forall$$e$:es{-}E(${\it es}$). 
\-\\[0ex]((loc($e$) = $i$) $\vee$ ($\uparrow$es{-}isrcv(${\it es}$; $e$)))
\\[0ex]$\Rightarrow$ (es{-}kind(${\it es}$; $e$) = $k$)
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); $T$))
\-\-\-
\end{tabbing}